0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 182 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 185 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 5 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 23 ms)
↳25 QDP
↳26 QDPOrderProof (⇔, 393 ms)
↳27 QDP
↳28 DependencyGraphProof (⇔, 0 ms)
↳29 TRUE
REVC_IN_GA(.(X1, .(X2, X3)), .(X4, X5)) → U11_GA(X1, X2, X3, X4, X5, rev1A_in_gga(X2, X3, X4))
REVC_IN_GA(.(X1, .(X2, X3)), .(X4, X5)) → REV1A_IN_GGA(X2, X3, X4)
REV1A_IN_GGA(X1, .(X2, X3), X4) → U1_GGA(X1, X2, X3, X4, rev1A_in_gga(X2, X3, X4))
REV1A_IN_GGA(X1, .(X2, X3), X4) → REV1A_IN_GGA(X2, X3, X4)
REVC_IN_GA(.(X1, .(X2, X3)), .(X4, X5)) → U12_GA(X1, X2, X3, X4, X5, rev1cA_in_gga(X2, X3, X4))
U12_GA(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → U13_GA(X1, X2, X3, X4, X5, rev2B_in_gga(X2, X3, X6))
U12_GA(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → REV2B_IN_GGA(X2, X3, X6)
REV2B_IN_GGA(X1, .(X2, X3), X4) → U2_GGA(X1, X2, X3, X4, rev2B_in_gga(X2, X3, X5))
REV2B_IN_GGA(X1, .(X2, X3), X4) → REV2B_IN_GGA(X2, X3, X5)
REV2B_IN_GGA(X1, .(X2, X3), X4) → U3_GGA(X1, X2, X3, X4, rev2cB_in_gga(X2, X3, X5))
U3_GGA(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → U4_GGA(X1, X2, X3, X4, revD_in_ga(X5, X6))
U3_GGA(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → REVD_IN_GA(X5, X6)
REVD_IN_GA(.(X1, X2), .(X3, X4)) → U8_GA(X1, X2, X3, X4, rev1E_in_gga(X1, X2, X3))
REVD_IN_GA(.(X1, X2), .(X3, X4)) → REV1E_IN_GGA(X1, X2, X3)
REV1E_IN_GGA(X1, .(X2, X3), X4) → U7_GGA(X1, X2, X3, X4, rev1E_in_gga(X2, X3, X4))
REV1E_IN_GGA(X1, .(X2, X3), X4) → REV1E_IN_GGA(X2, X3, X4)
REVD_IN_GA(.(X1, X2), .(X3, X4)) → U9_GA(X1, X2, X3, X4, rev1cE_in_gga(X1, X2, X3))
U9_GA(X1, X2, X3, X4, rev1cE_out_gga(X1, X2, X3)) → U10_GA(X1, X2, X3, X4, rev2B_in_gga(X1, X2, X4))
U9_GA(X1, X2, X3, X4, rev1cE_out_gga(X1, X2, X3)) → REV2B_IN_GGA(X1, X2, X4)
U3_GGA(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → U5_GGA(X1, X2, X3, X4, revcD_in_ga(X5, X6))
U5_GGA(X1, X2, X3, X4, revcD_out_ga(X5, X6)) → U6_GGA(X1, X2, X3, X4, revC_in_ga(.(X1, X6), X4))
U5_GGA(X1, X2, X3, X4, revcD_out_ga(X5, X6)) → REVC_IN_GA(.(X1, X6), X4)
U12_GA(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → U14_GA(X1, X2, X3, X4, X5, rev2cB_in_gga(X2, X3, X6))
U14_GA(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → U15_GA(X1, X2, X3, X4, X5, revD_in_ga(X6, X7))
U14_GA(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → REVD_IN_GA(X6, X7)
U14_GA(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → U16_GA(X1, X2, X3, X4, X5, revcD_in_ga(X6, X7))
U16_GA(X1, X2, X3, X4, X5, revcD_out_ga(X6, X7)) → U17_GA(X1, X2, X3, X4, X5, revC_in_ga(.(X1, X7), X5))
U16_GA(X1, X2, X3, X4, X5, revcD_out_ga(X6, X7)) → REVC_IN_GA(.(X1, X7), X5)
rev1cA_in_gga(X1, [], X1) → rev1cA_out_gga(X1, [], X1)
rev1cA_in_gga(X1, .(X2, X3), X4) → U19_gga(X1, X2, X3, X4, rev1cA_in_gga(X2, X3, X4))
U19_gga(X1, X2, X3, X4, rev1cA_out_gga(X2, X3, X4)) → rev1cA_out_gga(X1, .(X2, X3), X4)
rev2cB_in_gga(X1, [], []) → rev2cB_out_gga(X1, [], [])
rev2cB_in_gga(X1, .(X2, X3), X4) → U20_gga(X1, X2, X3, X4, rev2cB_in_gga(X2, X3, X5))
U20_gga(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → U21_gga(X1, X2, X3, X4, revcD_in_ga(X5, X6))
revcD_in_ga([], []) → revcD_out_ga([], [])
revcD_in_ga(.(X1, X2), .(X3, X4)) → U28_ga(X1, X2, X3, X4, rev1cE_in_gga(X1, X2, X3))
rev1cE_in_gga(X1, [], X1) → rev1cE_out_gga(X1, [], X1)
rev1cE_in_gga(X1, .(X2, X3), X4) → U27_gga(X1, X2, X3, X4, rev1cE_in_gga(X2, X3, X4))
U27_gga(X1, X2, X3, X4, rev1cE_out_gga(X2, X3, X4)) → rev1cE_out_gga(X1, .(X2, X3), X4)
U28_ga(X1, X2, X3, X4, rev1cE_out_gga(X1, X2, X3)) → U29_ga(X1, X2, X3, X4, rev2cB_in_gga(X1, X2, X4))
U29_ga(X1, X2, X3, X4, rev2cB_out_gga(X1, X2, X4)) → revcD_out_ga(.(X1, X2), .(X3, X4))
U21_gga(X1, X2, X3, X4, revcD_out_ga(X5, X6)) → U22_gga(X1, X2, X3, X4, revcC_in_ga(.(X1, X6), X4))
revcC_in_ga([], []) → revcC_out_ga([], [])
revcC_in_ga(.(X1, []), .(X1, [])) → revcC_out_ga(.(X1, []), .(X1, []))
revcC_in_ga(.(X1, .(X2, X3)), .(X4, X5)) → U23_ga(X1, X2, X3, X4, X5, rev1cA_in_gga(X2, X3, X4))
U23_ga(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → U24_ga(X1, X2, X3, X4, X5, rev2cB_in_gga(X2, X3, X6))
U24_ga(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → U25_ga(X1, X2, X3, X4, X5, revcD_in_ga(X6, X7))
U25_ga(X1, X2, X3, X4, X5, revcD_out_ga(X6, X7)) → U26_ga(X1, X2, X3, X4, X5, revcC_in_ga(.(X1, X7), X5))
U26_ga(X1, X2, X3, X4, X5, revcC_out_ga(.(X1, X7), X5)) → revcC_out_ga(.(X1, .(X2, X3)), .(X4, X5))
U22_gga(X1, X2, X3, X4, revcC_out_ga(.(X1, X6), X4)) → rev2cB_out_gga(X1, .(X2, X3), X4)
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
REVC_IN_GA(.(X1, .(X2, X3)), .(X4, X5)) → U11_GA(X1, X2, X3, X4, X5, rev1A_in_gga(X2, X3, X4))
REVC_IN_GA(.(X1, .(X2, X3)), .(X4, X5)) → REV1A_IN_GGA(X2, X3, X4)
REV1A_IN_GGA(X1, .(X2, X3), X4) → U1_GGA(X1, X2, X3, X4, rev1A_in_gga(X2, X3, X4))
REV1A_IN_GGA(X1, .(X2, X3), X4) → REV1A_IN_GGA(X2, X3, X4)
REVC_IN_GA(.(X1, .(X2, X3)), .(X4, X5)) → U12_GA(X1, X2, X3, X4, X5, rev1cA_in_gga(X2, X3, X4))
U12_GA(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → U13_GA(X1, X2, X3, X4, X5, rev2B_in_gga(X2, X3, X6))
U12_GA(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → REV2B_IN_GGA(X2, X3, X6)
REV2B_IN_GGA(X1, .(X2, X3), X4) → U2_GGA(X1, X2, X3, X4, rev2B_in_gga(X2, X3, X5))
REV2B_IN_GGA(X1, .(X2, X3), X4) → REV2B_IN_GGA(X2, X3, X5)
REV2B_IN_GGA(X1, .(X2, X3), X4) → U3_GGA(X1, X2, X3, X4, rev2cB_in_gga(X2, X3, X5))
U3_GGA(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → U4_GGA(X1, X2, X3, X4, revD_in_ga(X5, X6))
U3_GGA(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → REVD_IN_GA(X5, X6)
REVD_IN_GA(.(X1, X2), .(X3, X4)) → U8_GA(X1, X2, X3, X4, rev1E_in_gga(X1, X2, X3))
REVD_IN_GA(.(X1, X2), .(X3, X4)) → REV1E_IN_GGA(X1, X2, X3)
REV1E_IN_GGA(X1, .(X2, X3), X4) → U7_GGA(X1, X2, X3, X4, rev1E_in_gga(X2, X3, X4))
REV1E_IN_GGA(X1, .(X2, X3), X4) → REV1E_IN_GGA(X2, X3, X4)
REVD_IN_GA(.(X1, X2), .(X3, X4)) → U9_GA(X1, X2, X3, X4, rev1cE_in_gga(X1, X2, X3))
U9_GA(X1, X2, X3, X4, rev1cE_out_gga(X1, X2, X3)) → U10_GA(X1, X2, X3, X4, rev2B_in_gga(X1, X2, X4))
U9_GA(X1, X2, X3, X4, rev1cE_out_gga(X1, X2, X3)) → REV2B_IN_GGA(X1, X2, X4)
U3_GGA(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → U5_GGA(X1, X2, X3, X4, revcD_in_ga(X5, X6))
U5_GGA(X1, X2, X3, X4, revcD_out_ga(X5, X6)) → U6_GGA(X1, X2, X3, X4, revC_in_ga(.(X1, X6), X4))
U5_GGA(X1, X2, X3, X4, revcD_out_ga(X5, X6)) → REVC_IN_GA(.(X1, X6), X4)
U12_GA(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → U14_GA(X1, X2, X3, X4, X5, rev2cB_in_gga(X2, X3, X6))
U14_GA(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → U15_GA(X1, X2, X3, X4, X5, revD_in_ga(X6, X7))
U14_GA(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → REVD_IN_GA(X6, X7)
U14_GA(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → U16_GA(X1, X2, X3, X4, X5, revcD_in_ga(X6, X7))
U16_GA(X1, X2, X3, X4, X5, revcD_out_ga(X6, X7)) → U17_GA(X1, X2, X3, X4, X5, revC_in_ga(.(X1, X7), X5))
U16_GA(X1, X2, X3, X4, X5, revcD_out_ga(X6, X7)) → REVC_IN_GA(.(X1, X7), X5)
rev1cA_in_gga(X1, [], X1) → rev1cA_out_gga(X1, [], X1)
rev1cA_in_gga(X1, .(X2, X3), X4) → U19_gga(X1, X2, X3, X4, rev1cA_in_gga(X2, X3, X4))
U19_gga(X1, X2, X3, X4, rev1cA_out_gga(X2, X3, X4)) → rev1cA_out_gga(X1, .(X2, X3), X4)
rev2cB_in_gga(X1, [], []) → rev2cB_out_gga(X1, [], [])
rev2cB_in_gga(X1, .(X2, X3), X4) → U20_gga(X1, X2, X3, X4, rev2cB_in_gga(X2, X3, X5))
U20_gga(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → U21_gga(X1, X2, X3, X4, revcD_in_ga(X5, X6))
revcD_in_ga([], []) → revcD_out_ga([], [])
revcD_in_ga(.(X1, X2), .(X3, X4)) → U28_ga(X1, X2, X3, X4, rev1cE_in_gga(X1, X2, X3))
rev1cE_in_gga(X1, [], X1) → rev1cE_out_gga(X1, [], X1)
rev1cE_in_gga(X1, .(X2, X3), X4) → U27_gga(X1, X2, X3, X4, rev1cE_in_gga(X2, X3, X4))
U27_gga(X1, X2, X3, X4, rev1cE_out_gga(X2, X3, X4)) → rev1cE_out_gga(X1, .(X2, X3), X4)
U28_ga(X1, X2, X3, X4, rev1cE_out_gga(X1, X2, X3)) → U29_ga(X1, X2, X3, X4, rev2cB_in_gga(X1, X2, X4))
U29_ga(X1, X2, X3, X4, rev2cB_out_gga(X1, X2, X4)) → revcD_out_ga(.(X1, X2), .(X3, X4))
U21_gga(X1, X2, X3, X4, revcD_out_ga(X5, X6)) → U22_gga(X1, X2, X3, X4, revcC_in_ga(.(X1, X6), X4))
revcC_in_ga([], []) → revcC_out_ga([], [])
revcC_in_ga(.(X1, []), .(X1, [])) → revcC_out_ga(.(X1, []), .(X1, []))
revcC_in_ga(.(X1, .(X2, X3)), .(X4, X5)) → U23_ga(X1, X2, X3, X4, X5, rev1cA_in_gga(X2, X3, X4))
U23_ga(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → U24_ga(X1, X2, X3, X4, X5, rev2cB_in_gga(X2, X3, X6))
U24_ga(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → U25_ga(X1, X2, X3, X4, X5, revcD_in_ga(X6, X7))
U25_ga(X1, X2, X3, X4, X5, revcD_out_ga(X6, X7)) → U26_ga(X1, X2, X3, X4, X5, revcC_in_ga(.(X1, X7), X5))
U26_ga(X1, X2, X3, X4, X5, revcC_out_ga(.(X1, X7), X5)) → revcC_out_ga(.(X1, .(X2, X3)), .(X4, X5))
U22_gga(X1, X2, X3, X4, revcC_out_ga(.(X1, X6), X4)) → rev2cB_out_gga(X1, .(X2, X3), X4)
REV1E_IN_GGA(X1, .(X2, X3), X4) → REV1E_IN_GGA(X2, X3, X4)
rev1cA_in_gga(X1, [], X1) → rev1cA_out_gga(X1, [], X1)
rev1cA_in_gga(X1, .(X2, X3), X4) → U19_gga(X1, X2, X3, X4, rev1cA_in_gga(X2, X3, X4))
U19_gga(X1, X2, X3, X4, rev1cA_out_gga(X2, X3, X4)) → rev1cA_out_gga(X1, .(X2, X3), X4)
rev2cB_in_gga(X1, [], []) → rev2cB_out_gga(X1, [], [])
rev2cB_in_gga(X1, .(X2, X3), X4) → U20_gga(X1, X2, X3, X4, rev2cB_in_gga(X2, X3, X5))
U20_gga(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → U21_gga(X1, X2, X3, X4, revcD_in_ga(X5, X6))
revcD_in_ga([], []) → revcD_out_ga([], [])
revcD_in_ga(.(X1, X2), .(X3, X4)) → U28_ga(X1, X2, X3, X4, rev1cE_in_gga(X1, X2, X3))
rev1cE_in_gga(X1, [], X1) → rev1cE_out_gga(X1, [], X1)
rev1cE_in_gga(X1, .(X2, X3), X4) → U27_gga(X1, X2, X3, X4, rev1cE_in_gga(X2, X3, X4))
U27_gga(X1, X2, X3, X4, rev1cE_out_gga(X2, X3, X4)) → rev1cE_out_gga(X1, .(X2, X3), X4)
U28_ga(X1, X2, X3, X4, rev1cE_out_gga(X1, X2, X3)) → U29_ga(X1, X2, X3, X4, rev2cB_in_gga(X1, X2, X4))
U29_ga(X1, X2, X3, X4, rev2cB_out_gga(X1, X2, X4)) → revcD_out_ga(.(X1, X2), .(X3, X4))
U21_gga(X1, X2, X3, X4, revcD_out_ga(X5, X6)) → U22_gga(X1, X2, X3, X4, revcC_in_ga(.(X1, X6), X4))
revcC_in_ga([], []) → revcC_out_ga([], [])
revcC_in_ga(.(X1, []), .(X1, [])) → revcC_out_ga(.(X1, []), .(X1, []))
revcC_in_ga(.(X1, .(X2, X3)), .(X4, X5)) → U23_ga(X1, X2, X3, X4, X5, rev1cA_in_gga(X2, X3, X4))
U23_ga(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → U24_ga(X1, X2, X3, X4, X5, rev2cB_in_gga(X2, X3, X6))
U24_ga(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → U25_ga(X1, X2, X3, X4, X5, revcD_in_ga(X6, X7))
U25_ga(X1, X2, X3, X4, X5, revcD_out_ga(X6, X7)) → U26_ga(X1, X2, X3, X4, X5, revcC_in_ga(.(X1, X7), X5))
U26_ga(X1, X2, X3, X4, X5, revcC_out_ga(.(X1, X7), X5)) → revcC_out_ga(.(X1, .(X2, X3)), .(X4, X5))
U22_gga(X1, X2, X3, X4, revcC_out_ga(.(X1, X6), X4)) → rev2cB_out_gga(X1, .(X2, X3), X4)
REV1E_IN_GGA(X1, .(X2, X3), X4) → REV1E_IN_GGA(X2, X3, X4)
REV1E_IN_GGA(X1, .(X2, X3)) → REV1E_IN_GGA(X2, X3)
From the DPs we obtained the following set of size-change graphs:
REV1A_IN_GGA(X1, .(X2, X3), X4) → REV1A_IN_GGA(X2, X3, X4)
rev1cA_in_gga(X1, [], X1) → rev1cA_out_gga(X1, [], X1)
rev1cA_in_gga(X1, .(X2, X3), X4) → U19_gga(X1, X2, X3, X4, rev1cA_in_gga(X2, X3, X4))
U19_gga(X1, X2, X3, X4, rev1cA_out_gga(X2, X3, X4)) → rev1cA_out_gga(X1, .(X2, X3), X4)
rev2cB_in_gga(X1, [], []) → rev2cB_out_gga(X1, [], [])
rev2cB_in_gga(X1, .(X2, X3), X4) → U20_gga(X1, X2, X3, X4, rev2cB_in_gga(X2, X3, X5))
U20_gga(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → U21_gga(X1, X2, X3, X4, revcD_in_ga(X5, X6))
revcD_in_ga([], []) → revcD_out_ga([], [])
revcD_in_ga(.(X1, X2), .(X3, X4)) → U28_ga(X1, X2, X3, X4, rev1cE_in_gga(X1, X2, X3))
rev1cE_in_gga(X1, [], X1) → rev1cE_out_gga(X1, [], X1)
rev1cE_in_gga(X1, .(X2, X3), X4) → U27_gga(X1, X2, X3, X4, rev1cE_in_gga(X2, X3, X4))
U27_gga(X1, X2, X3, X4, rev1cE_out_gga(X2, X3, X4)) → rev1cE_out_gga(X1, .(X2, X3), X4)
U28_ga(X1, X2, X3, X4, rev1cE_out_gga(X1, X2, X3)) → U29_ga(X1, X2, X3, X4, rev2cB_in_gga(X1, X2, X4))
U29_ga(X1, X2, X3, X4, rev2cB_out_gga(X1, X2, X4)) → revcD_out_ga(.(X1, X2), .(X3, X4))
U21_gga(X1, X2, X3, X4, revcD_out_ga(X5, X6)) → U22_gga(X1, X2, X3, X4, revcC_in_ga(.(X1, X6), X4))
revcC_in_ga([], []) → revcC_out_ga([], [])
revcC_in_ga(.(X1, []), .(X1, [])) → revcC_out_ga(.(X1, []), .(X1, []))
revcC_in_ga(.(X1, .(X2, X3)), .(X4, X5)) → U23_ga(X1, X2, X3, X4, X5, rev1cA_in_gga(X2, X3, X4))
U23_ga(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → U24_ga(X1, X2, X3, X4, X5, rev2cB_in_gga(X2, X3, X6))
U24_ga(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → U25_ga(X1, X2, X3, X4, X5, revcD_in_ga(X6, X7))
U25_ga(X1, X2, X3, X4, X5, revcD_out_ga(X6, X7)) → U26_ga(X1, X2, X3, X4, X5, revcC_in_ga(.(X1, X7), X5))
U26_ga(X1, X2, X3, X4, X5, revcC_out_ga(.(X1, X7), X5)) → revcC_out_ga(.(X1, .(X2, X3)), .(X4, X5))
U22_gga(X1, X2, X3, X4, revcC_out_ga(.(X1, X6), X4)) → rev2cB_out_gga(X1, .(X2, X3), X4)
REV1A_IN_GGA(X1, .(X2, X3), X4) → REV1A_IN_GGA(X2, X3, X4)
REV1A_IN_GGA(X1, .(X2, X3)) → REV1A_IN_GGA(X2, X3)
From the DPs we obtained the following set of size-change graphs:
REVC_IN_GA(.(X1, .(X2, X3)), .(X4, X5)) → U12_GA(X1, X2, X3, X4, X5, rev1cA_in_gga(X2, X3, X4))
U12_GA(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → REV2B_IN_GGA(X2, X3, X6)
REV2B_IN_GGA(X1, .(X2, X3), X4) → REV2B_IN_GGA(X2, X3, X5)
REV2B_IN_GGA(X1, .(X2, X3), X4) → U3_GGA(X1, X2, X3, X4, rev2cB_in_gga(X2, X3, X5))
U3_GGA(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → REVD_IN_GA(X5, X6)
REVD_IN_GA(.(X1, X2), .(X3, X4)) → U9_GA(X1, X2, X3, X4, rev1cE_in_gga(X1, X2, X3))
U9_GA(X1, X2, X3, X4, rev1cE_out_gga(X1, X2, X3)) → REV2B_IN_GGA(X1, X2, X4)
U3_GGA(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → U5_GGA(X1, X2, X3, X4, revcD_in_ga(X5, X6))
U5_GGA(X1, X2, X3, X4, revcD_out_ga(X5, X6)) → REVC_IN_GA(.(X1, X6), X4)
U12_GA(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → U14_GA(X1, X2, X3, X4, X5, rev2cB_in_gga(X2, X3, X6))
U14_GA(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → REVD_IN_GA(X6, X7)
U14_GA(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → U16_GA(X1, X2, X3, X4, X5, revcD_in_ga(X6, X7))
U16_GA(X1, X2, X3, X4, X5, revcD_out_ga(X6, X7)) → REVC_IN_GA(.(X1, X7), X5)
rev1cA_in_gga(X1, [], X1) → rev1cA_out_gga(X1, [], X1)
rev1cA_in_gga(X1, .(X2, X3), X4) → U19_gga(X1, X2, X3, X4, rev1cA_in_gga(X2, X3, X4))
U19_gga(X1, X2, X3, X4, rev1cA_out_gga(X2, X3, X4)) → rev1cA_out_gga(X1, .(X2, X3), X4)
rev2cB_in_gga(X1, [], []) → rev2cB_out_gga(X1, [], [])
rev2cB_in_gga(X1, .(X2, X3), X4) → U20_gga(X1, X2, X3, X4, rev2cB_in_gga(X2, X3, X5))
U20_gga(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → U21_gga(X1, X2, X3, X4, revcD_in_ga(X5, X6))
revcD_in_ga([], []) → revcD_out_ga([], [])
revcD_in_ga(.(X1, X2), .(X3, X4)) → U28_ga(X1, X2, X3, X4, rev1cE_in_gga(X1, X2, X3))
rev1cE_in_gga(X1, [], X1) → rev1cE_out_gga(X1, [], X1)
rev1cE_in_gga(X1, .(X2, X3), X4) → U27_gga(X1, X2, X3, X4, rev1cE_in_gga(X2, X3, X4))
U27_gga(X1, X2, X3, X4, rev1cE_out_gga(X2, X3, X4)) → rev1cE_out_gga(X1, .(X2, X3), X4)
U28_ga(X1, X2, X3, X4, rev1cE_out_gga(X1, X2, X3)) → U29_ga(X1, X2, X3, X4, rev2cB_in_gga(X1, X2, X4))
U29_ga(X1, X2, X3, X4, rev2cB_out_gga(X1, X2, X4)) → revcD_out_ga(.(X1, X2), .(X3, X4))
U21_gga(X1, X2, X3, X4, revcD_out_ga(X5, X6)) → U22_gga(X1, X2, X3, X4, revcC_in_ga(.(X1, X6), X4))
revcC_in_ga([], []) → revcC_out_ga([], [])
revcC_in_ga(.(X1, []), .(X1, [])) → revcC_out_ga(.(X1, []), .(X1, []))
revcC_in_ga(.(X1, .(X2, X3)), .(X4, X5)) → U23_ga(X1, X2, X3, X4, X5, rev1cA_in_gga(X2, X3, X4))
U23_ga(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → U24_ga(X1, X2, X3, X4, X5, rev2cB_in_gga(X2, X3, X6))
U24_ga(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → U25_ga(X1, X2, X3, X4, X5, revcD_in_ga(X6, X7))
U25_ga(X1, X2, X3, X4, X5, revcD_out_ga(X6, X7)) → U26_ga(X1, X2, X3, X4, X5, revcC_in_ga(.(X1, X7), X5))
U26_ga(X1, X2, X3, X4, X5, revcC_out_ga(.(X1, X7), X5)) → revcC_out_ga(.(X1, .(X2, X3)), .(X4, X5))
U22_gga(X1, X2, X3, X4, revcC_out_ga(.(X1, X6), X4)) → rev2cB_out_gga(X1, .(X2, X3), X4)
REVC_IN_GA(.(X1, .(X2, X3)), .(X4, X5)) → U12_GA(X1, X2, X3, X4, X5, rev1cA_in_gga(X2, X3, X4))
U12_GA(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → REV2B_IN_GGA(X2, X3, X6)
REV2B_IN_GGA(X1, .(X2, X3), X4) → REV2B_IN_GGA(X2, X3, X5)
REV2B_IN_GGA(X1, .(X2, X3), X4) → U3_GGA(X1, X2, X3, X4, rev2cB_in_gga(X2, X3, X5))
U3_GGA(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → REVD_IN_GA(X5, X6)
REVD_IN_GA(.(X1, X2), .(X3, X4)) → U9_GA(X1, X2, X3, X4, rev1cE_in_gga(X1, X2, X3))
U9_GA(X1, X2, X3, X4, rev1cE_out_gga(X1, X2, X3)) → REV2B_IN_GGA(X1, X2, X4)
U3_GGA(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → U5_GGA(X1, X2, X3, X4, revcD_in_ga(X5, X6))
U5_GGA(X1, X2, X3, X4, revcD_out_ga(X5, X6)) → REVC_IN_GA(.(X1, X6), X4)
U12_GA(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → U14_GA(X1, X2, X3, X4, X5, rev2cB_in_gga(X2, X3, X6))
U14_GA(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → REVD_IN_GA(X6, X7)
U14_GA(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → U16_GA(X1, X2, X3, X4, X5, revcD_in_ga(X6, X7))
U16_GA(X1, X2, X3, X4, X5, revcD_out_ga(X6, X7)) → REVC_IN_GA(.(X1, X7), X5)
rev1cA_in_gga(X1, [], X1) → rev1cA_out_gga(X1, [], X1)
rev1cA_in_gga(X1, .(X2, X3), X4) → U19_gga(X1, X2, X3, X4, rev1cA_in_gga(X2, X3, X4))
rev2cB_in_gga(X1, [], []) → rev2cB_out_gga(X1, [], [])
rev2cB_in_gga(X1, .(X2, X3), X4) → U20_gga(X1, X2, X3, X4, rev2cB_in_gga(X2, X3, X5))
rev1cE_in_gga(X1, [], X1) → rev1cE_out_gga(X1, [], X1)
rev1cE_in_gga(X1, .(X2, X3), X4) → U27_gga(X1, X2, X3, X4, rev1cE_in_gga(X2, X3, X4))
revcD_in_ga([], []) → revcD_out_ga([], [])
revcD_in_ga(.(X1, X2), .(X3, X4)) → U28_ga(X1, X2, X3, X4, rev1cE_in_gga(X1, X2, X3))
U19_gga(X1, X2, X3, X4, rev1cA_out_gga(X2, X3, X4)) → rev1cA_out_gga(X1, .(X2, X3), X4)
U20_gga(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X5)) → U21_gga(X1, X2, X3, X4, revcD_in_ga(X5, X6))
U27_gga(X1, X2, X3, X4, rev1cE_out_gga(X2, X3, X4)) → rev1cE_out_gga(X1, .(X2, X3), X4)
U28_ga(X1, X2, X3, X4, rev1cE_out_gga(X1, X2, X3)) → U29_ga(X1, X2, X3, X4, rev2cB_in_gga(X1, X2, X4))
U21_gga(X1, X2, X3, X4, revcD_out_ga(X5, X6)) → U22_gga(X1, X2, X3, X4, revcC_in_ga(.(X1, X6), X4))
U29_ga(X1, X2, X3, X4, rev2cB_out_gga(X1, X2, X4)) → revcD_out_ga(.(X1, X2), .(X3, X4))
U22_gga(X1, X2, X3, X4, revcC_out_ga(.(X1, X6), X4)) → rev2cB_out_gga(X1, .(X2, X3), X4)
revcC_in_ga(.(X1, []), .(X1, [])) → revcC_out_ga(.(X1, []), .(X1, []))
revcC_in_ga(.(X1, .(X2, X3)), .(X4, X5)) → U23_ga(X1, X2, X3, X4, X5, rev1cA_in_gga(X2, X3, X4))
U23_ga(X1, X2, X3, X4, X5, rev1cA_out_gga(X2, X3, X4)) → U24_ga(X1, X2, X3, X4, X5, rev2cB_in_gga(X2, X3, X6))
U24_ga(X1, X2, X3, X4, X5, rev2cB_out_gga(X2, X3, X6)) → U25_ga(X1, X2, X3, X4, X5, revcD_in_ga(X6, X7))
U25_ga(X1, X2, X3, X4, X5, revcD_out_ga(X6, X7)) → U26_ga(X1, X2, X3, X4, X5, revcC_in_ga(.(X1, X7), X5))
U26_ga(X1, X2, X3, X4, X5, revcC_out_ga(.(X1, X7), X5)) → revcC_out_ga(.(X1, .(X2, X3)), .(X4, X5))
REVC_IN_GA(.(X1, .(X2, X3))) → U12_GA(X1, X2, X3, rev1cA_in_gga(X2, X3))
U12_GA(X1, X2, X3, rev1cA_out_gga(X2, X3, X4)) → REV2B_IN_GGA(X2, X3)
REV2B_IN_GGA(X1, .(X2, X3)) → REV2B_IN_GGA(X2, X3)
REV2B_IN_GGA(X1, .(X2, X3)) → U3_GGA(X1, X2, X3, rev2cB_in_gga(X2, X3))
U3_GGA(X1, X2, X3, rev2cB_out_gga(X2, X3, X5)) → REVD_IN_GA(X5)
REVD_IN_GA(.(X1, X2)) → U9_GA(X1, X2, rev1cE_in_gga(X1, X2))
U9_GA(X1, X2, rev1cE_out_gga(X1, X2, X3)) → REV2B_IN_GGA(X1, X2)
U3_GGA(X1, X2, X3, rev2cB_out_gga(X2, X3, X5)) → U5_GGA(X1, X2, X3, revcD_in_ga(X5))
U5_GGA(X1, X2, X3, revcD_out_ga(X5, X6)) → REVC_IN_GA(.(X1, X6))
U12_GA(X1, X2, X3, rev1cA_out_gga(X2, X3, X4)) → U14_GA(X1, X2, X3, rev2cB_in_gga(X2, X3))
U14_GA(X1, X2, X3, rev2cB_out_gga(X2, X3, X6)) → REVD_IN_GA(X6)
U14_GA(X1, X2, X3, rev2cB_out_gga(X2, X3, X6)) → U16_GA(X1, X2, X3, revcD_in_ga(X6))
U16_GA(X1, X2, X3, revcD_out_ga(X6, X7)) → REVC_IN_GA(.(X1, X7))
rev1cA_in_gga(X1, []) → rev1cA_out_gga(X1, [], X1)
rev1cA_in_gga(X1, .(X2, X3)) → U19_gga(X1, X2, X3, rev1cA_in_gga(X2, X3))
rev2cB_in_gga(X1, []) → rev2cB_out_gga(X1, [], [])
rev2cB_in_gga(X1, .(X2, X3)) → U20_gga(X1, X2, X3, rev2cB_in_gga(X2, X3))
rev1cE_in_gga(X1, []) → rev1cE_out_gga(X1, [], X1)
rev1cE_in_gga(X1, .(X2, X3)) → U27_gga(X1, X2, X3, rev1cE_in_gga(X2, X3))
revcD_in_ga([]) → revcD_out_ga([], [])
revcD_in_ga(.(X1, X2)) → U28_ga(X1, X2, rev1cE_in_gga(X1, X2))
U19_gga(X1, X2, X3, rev1cA_out_gga(X2, X3, X4)) → rev1cA_out_gga(X1, .(X2, X3), X4)
U20_gga(X1, X2, X3, rev2cB_out_gga(X2, X3, X5)) → U21_gga(X1, X2, X3, revcD_in_ga(X5))
U27_gga(X1, X2, X3, rev1cE_out_gga(X2, X3, X4)) → rev1cE_out_gga(X1, .(X2, X3), X4)
U28_ga(X1, X2, rev1cE_out_gga(X1, X2, X3)) → U29_ga(X1, X2, X3, rev2cB_in_gga(X1, X2))
U21_gga(X1, X2, X3, revcD_out_ga(X5, X6)) → U22_gga(X1, X2, X3, revcC_in_ga(.(X1, X6)))
U29_ga(X1, X2, X3, rev2cB_out_gga(X1, X2, X4)) → revcD_out_ga(.(X1, X2), .(X3, X4))
U22_gga(X1, X2, X3, revcC_out_ga(.(X1, X6), X4)) → rev2cB_out_gga(X1, .(X2, X3), X4)
revcC_in_ga(.(X1, [])) → revcC_out_ga(.(X1, []), .(X1, []))
revcC_in_ga(.(X1, .(X2, X3))) → U23_ga(X1, X2, X3, rev1cA_in_gga(X2, X3))
U23_ga(X1, X2, X3, rev1cA_out_gga(X2, X3, X4)) → U24_ga(X1, X2, X3, X4, rev2cB_in_gga(X2, X3))
U24_ga(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X6)) → U25_ga(X1, X2, X3, X4, revcD_in_ga(X6))
U25_ga(X1, X2, X3, X4, revcD_out_ga(X6, X7)) → U26_ga(X1, X2, X3, X4, revcC_in_ga(.(X1, X7)))
U26_ga(X1, X2, X3, X4, revcC_out_ga(.(X1, X7), X5)) → revcC_out_ga(.(X1, .(X2, X3)), .(X4, X5))
rev1cA_in_gga(x0, x1)
rev2cB_in_gga(x0, x1)
rev1cE_in_gga(x0, x1)
revcD_in_ga(x0)
U19_gga(x0, x1, x2, x3)
U20_gga(x0, x1, x2, x3)
U27_gga(x0, x1, x2, x3)
U28_ga(x0, x1, x2)
U21_gga(x0, x1, x2, x3)
U29_ga(x0, x1, x2, x3)
U22_gga(x0, x1, x2, x3)
revcC_in_ga(x0)
U23_ga(x0, x1, x2, x3)
U24_ga(x0, x1, x2, x3, x4)
U25_ga(x0, x1, x2, x3, x4)
U26_ga(x0, x1, x2, x3, x4)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
REVC_IN_GA(.(X1, .(X2, X3))) → U12_GA(X1, X2, X3, rev1cA_in_gga(X2, X3))
REV2B_IN_GGA(X1, .(X2, X3)) → REV2B_IN_GGA(X2, X3)
U3_GGA(X1, X2, X3, rev2cB_out_gga(X2, X3, X5)) → REVD_IN_GA(X5)
U3_GGA(X1, X2, X3, rev2cB_out_gga(X2, X3, X5)) → U5_GGA(X1, X2, X3, revcD_in_ga(X5))
U14_GA(X1, X2, X3, rev2cB_out_gga(X2, X3, X6)) → REVD_IN_GA(X6)
POL(.(x1, x2)) = 1 + x2
POL(REV2B_IN_GGA(x1, x2)) = 1 + x2
POL(REVC_IN_GA(x1)) = x1
POL(REVD_IN_GA(x1)) = x1
POL(U12_GA(x1, x2, x3, x4)) = 1 + x3
POL(U14_GA(x1, x2, x3, x4)) = x4
POL(U16_GA(x1, x2, x3, x4)) = x4
POL(U19_gga(x1, x2, x3, x4)) = 1
POL(U20_gga(x1, x2, x3, x4)) = 1 + x4
POL(U21_gga(x1, x2, x3, x4)) = 1 + x4
POL(U22_gga(x1, x2, x3, x4)) = 1 + x4
POL(U23_ga(x1, x2, x3, x4)) = 1 + x3 + x4
POL(U24_ga(x1, x2, x3, x4, x5)) = 1 + x5
POL(U25_ga(x1, x2, x3, x4, x5)) = 1 + x5
POL(U26_ga(x1, x2, x3, x4, x5)) = 1 + x5
POL(U27_gga(x1, x2, x3, x4)) = 1
POL(U28_ga(x1, x2, x3)) = 1 + x2 + x3
POL(U29_ga(x1, x2, x3, x4)) = 1 + x4
POL(U3_GGA(x1, x2, x3, x4)) = 1 + x4
POL(U5_GGA(x1, x2, x3, x4)) = x4
POL(U9_GA(x1, x2, x3)) = 1 + x2
POL([]) = 0
POL(rev1cA_in_gga(x1, x2)) = 1
POL(rev1cA_out_gga(x1, x2, x3)) = 1
POL(rev1cE_in_gga(x1, x2)) = 1
POL(rev1cE_out_gga(x1, x2, x3)) = 1
POL(rev2cB_in_gga(x1, x2)) = 1 + x2
POL(rev2cB_out_gga(x1, x2, x3)) = 1 + x3
POL(revcC_in_ga(x1)) = x1
POL(revcC_out_ga(x1, x2)) = x2
POL(revcD_in_ga(x1)) = 1 + x1
POL(revcD_out_ga(x1, x2)) = 1 + x2
rev1cA_in_gga(X1, []) → rev1cA_out_gga(X1, [], X1)
rev1cA_in_gga(X1, .(X2, X3)) → U19_gga(X1, X2, X3, rev1cA_in_gga(X2, X3))
rev2cB_in_gga(X1, []) → rev2cB_out_gga(X1, [], [])
rev2cB_in_gga(X1, .(X2, X3)) → U20_gga(X1, X2, X3, rev2cB_in_gga(X2, X3))
rev1cE_in_gga(X1, []) → rev1cE_out_gga(X1, [], X1)
rev1cE_in_gga(X1, .(X2, X3)) → U27_gga(X1, X2, X3, rev1cE_in_gga(X2, X3))
revcD_in_ga([]) → revcD_out_ga([], [])
revcD_in_ga(.(X1, X2)) → U28_ga(X1, X2, rev1cE_in_gga(X1, X2))
U23_ga(X1, X2, X3, rev1cA_out_gga(X2, X3, X4)) → U24_ga(X1, X2, X3, X4, rev2cB_in_gga(X2, X3))
U20_gga(X1, X2, X3, rev2cB_out_gga(X2, X3, X5)) → U21_gga(X1, X2, X3, revcD_in_ga(X5))
U28_ga(X1, X2, rev1cE_out_gga(X1, X2, X3)) → U29_ga(X1, X2, X3, rev2cB_in_gga(X1, X2))
U29_ga(X1, X2, X3, rev2cB_out_gga(X1, X2, X4)) → revcD_out_ga(.(X1, X2), .(X3, X4))
U21_gga(X1, X2, X3, revcD_out_ga(X5, X6)) → U22_gga(X1, X2, X3, revcC_in_ga(.(X1, X6)))
revcC_in_ga(.(X1, [])) → revcC_out_ga(.(X1, []), .(X1, []))
U22_gga(X1, X2, X3, revcC_out_ga(.(X1, X6), X4)) → rev2cB_out_gga(X1, .(X2, X3), X4)
revcC_in_ga(.(X1, .(X2, X3))) → U23_ga(X1, X2, X3, rev1cA_in_gga(X2, X3))
U24_ga(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X6)) → U25_ga(X1, X2, X3, X4, revcD_in_ga(X6))
U25_ga(X1, X2, X3, X4, revcD_out_ga(X6, X7)) → U26_ga(X1, X2, X3, X4, revcC_in_ga(.(X1, X7)))
U26_ga(X1, X2, X3, X4, revcC_out_ga(.(X1, X7), X5)) → revcC_out_ga(.(X1, .(X2, X3)), .(X4, X5))
U19_gga(X1, X2, X3, rev1cA_out_gga(X2, X3, X4)) → rev1cA_out_gga(X1, .(X2, X3), X4)
U27_gga(X1, X2, X3, rev1cE_out_gga(X2, X3, X4)) → rev1cE_out_gga(X1, .(X2, X3), X4)
U12_GA(X1, X2, X3, rev1cA_out_gga(X2, X3, X4)) → REV2B_IN_GGA(X2, X3)
REV2B_IN_GGA(X1, .(X2, X3)) → U3_GGA(X1, X2, X3, rev2cB_in_gga(X2, X3))
REVD_IN_GA(.(X1, X2)) → U9_GA(X1, X2, rev1cE_in_gga(X1, X2))
U9_GA(X1, X2, rev1cE_out_gga(X1, X2, X3)) → REV2B_IN_GGA(X1, X2)
U5_GGA(X1, X2, X3, revcD_out_ga(X5, X6)) → REVC_IN_GA(.(X1, X6))
U12_GA(X1, X2, X3, rev1cA_out_gga(X2, X3, X4)) → U14_GA(X1, X2, X3, rev2cB_in_gga(X2, X3))
U14_GA(X1, X2, X3, rev2cB_out_gga(X2, X3, X6)) → U16_GA(X1, X2, X3, revcD_in_ga(X6))
U16_GA(X1, X2, X3, revcD_out_ga(X6, X7)) → REVC_IN_GA(.(X1, X7))
rev1cA_in_gga(X1, []) → rev1cA_out_gga(X1, [], X1)
rev1cA_in_gga(X1, .(X2, X3)) → U19_gga(X1, X2, X3, rev1cA_in_gga(X2, X3))
rev2cB_in_gga(X1, []) → rev2cB_out_gga(X1, [], [])
rev2cB_in_gga(X1, .(X2, X3)) → U20_gga(X1, X2, X3, rev2cB_in_gga(X2, X3))
rev1cE_in_gga(X1, []) → rev1cE_out_gga(X1, [], X1)
rev1cE_in_gga(X1, .(X2, X3)) → U27_gga(X1, X2, X3, rev1cE_in_gga(X2, X3))
revcD_in_ga([]) → revcD_out_ga([], [])
revcD_in_ga(.(X1, X2)) → U28_ga(X1, X2, rev1cE_in_gga(X1, X2))
U19_gga(X1, X2, X3, rev1cA_out_gga(X2, X3, X4)) → rev1cA_out_gga(X1, .(X2, X3), X4)
U20_gga(X1, X2, X3, rev2cB_out_gga(X2, X3, X5)) → U21_gga(X1, X2, X3, revcD_in_ga(X5))
U27_gga(X1, X2, X3, rev1cE_out_gga(X2, X3, X4)) → rev1cE_out_gga(X1, .(X2, X3), X4)
U28_ga(X1, X2, rev1cE_out_gga(X1, X2, X3)) → U29_ga(X1, X2, X3, rev2cB_in_gga(X1, X2))
U21_gga(X1, X2, X3, revcD_out_ga(X5, X6)) → U22_gga(X1, X2, X3, revcC_in_ga(.(X1, X6)))
U29_ga(X1, X2, X3, rev2cB_out_gga(X1, X2, X4)) → revcD_out_ga(.(X1, X2), .(X3, X4))
U22_gga(X1, X2, X3, revcC_out_ga(.(X1, X6), X4)) → rev2cB_out_gga(X1, .(X2, X3), X4)
revcC_in_ga(.(X1, [])) → revcC_out_ga(.(X1, []), .(X1, []))
revcC_in_ga(.(X1, .(X2, X3))) → U23_ga(X1, X2, X3, rev1cA_in_gga(X2, X3))
U23_ga(X1, X2, X3, rev1cA_out_gga(X2, X3, X4)) → U24_ga(X1, X2, X3, X4, rev2cB_in_gga(X2, X3))
U24_ga(X1, X2, X3, X4, rev2cB_out_gga(X2, X3, X6)) → U25_ga(X1, X2, X3, X4, revcD_in_ga(X6))
U25_ga(X1, X2, X3, X4, revcD_out_ga(X6, X7)) → U26_ga(X1, X2, X3, X4, revcC_in_ga(.(X1, X7)))
U26_ga(X1, X2, X3, X4, revcC_out_ga(.(X1, X7), X5)) → revcC_out_ga(.(X1, .(X2, X3)), .(X4, X5))
rev1cA_in_gga(x0, x1)
rev2cB_in_gga(x0, x1)
rev1cE_in_gga(x0, x1)
revcD_in_ga(x0)
U19_gga(x0, x1, x2, x3)
U20_gga(x0, x1, x2, x3)
U27_gga(x0, x1, x2, x3)
U28_ga(x0, x1, x2)
U21_gga(x0, x1, x2, x3)
U29_ga(x0, x1, x2, x3)
U22_gga(x0, x1, x2, x3)
revcC_in_ga(x0)
U23_ga(x0, x1, x2, x3)
U24_ga(x0, x1, x2, x3, x4)
U25_ga(x0, x1, x2, x3, x4)
U26_ga(x0, x1, x2, x3, x4)